D:Dsys. D  D 

latex

Definitions	D1  D2, M1  M2, Id, Dsys, P  Q, M(i), x:A. B(x), t  T
Lemmas	d-m wf, ma-sub weakening, dsys wf, Id wf